perm filename YY[BNF,JRA] blob sn#045423 filedate 1973-05-25 generic text, type T, neo UTF8
00100	
00300	
00400	<AXIOM> ::=<NAME><ASSUM><DRECUR><INEQ><BODY>    =>[(PROG
00500							    (LSTNAME)
00600							    (SETQ
00700							     LSTNAME
00800							     (READLIST(APPEND LST(EXPLODE(STK4)))))
00900							    (RETURN
01000							     (LIST
01100							      (QUOTE DEFPROP)
01200							      (STK4)
01300							      (CONS
01400							       (QUOTE THCONSE)
01500							       (CONS
01600								(APPEND
01700								 (UNION POSTLIST PRELIST)
01800								 (LIST
01900								  (QUOTE CGL)
02000								  (LIST
02100								   LSTNAME
02200								   (LIST(QUOTE QUOTE)POSTLIST))))
02300								(APPEND
02400								 (CDR(STK0))
02500								 (QUOTE
02600								  ((THSETQ(THV LCTR)(THV GCTR))))
02700								 (COND
02800								  ((NULL(STK2))
02900								   (LIST
03000								    (LIST(QUOTE THUNIQUE)LSTNAME))))
03100								 (LIST
03200								  (LIST
03300								   (QUOTE TREEPATH)
03400								   (STK4)
03500								   (CADR(STK0)))
03600								  (QUOTE(TRACEINFO1))
03700								  (LIST
03800								   (QUOTE THOR)
03900								   T
04000								   (LIST(QUOTE TRACEINFO2)(STK4)))
04100								  (QUOTE(COND((TTYIN)(ADVICESYS)))))
04200								 (COND
04300								  ((EQ(CAAR(STK0))(QUOTE THAND))
04400								   (CDAR(STK0)))
04500								  (T(LIST(CAR(STK0)))))
04600								 (QUOTE
04700								  ((THSETQ
04800								    (THV DBLITS)
04900								    (CONS(CDAR CT)(THV DBLITS)))
05000								   (COND
05100								    ((EQ(QUOTE IF)(CADAR CT))
05200								     (ELSECLAUSE))
05300								    (T(THSETQ CT(CDR CT)T T))))))))
05400							      (QUOTE THEOREM))))]
05500	
05600	<NAME>  ::=<ID>					=>[(PROG2
05700							    (SETQ
05800							     VARLIST
05900							     (SETQ POSTLIST(SETQ PRELIST NIL)))
06000							    (STK0))]
06100	
06200	<ASSUM> ::=T					=>T
06300		::=NIL					=>NIL
06400	
06500	<DRECUR>::=T					=>T
06600		::=NIL					=>NIL
06700	
06800	<INEQ>  ::=NIL					=>NIL
06900		::=(<INARGS>				=>*
07000	
07100	<INARGS>::=<INARG>,<INARGS>			=>(INARG.INARGS)
07200		::=<INARG>)				=>(INARG)
07300	
07400	<INARG> ::=X					=>X
07500		::=⊗					=>⊗
07600	
07700	<BODY>  ::=<PRECONDS><POSTCOND>			=>[(PROG2
07800							    (SETQ POSTLIST VARLIST)
07900							    (CONS(STK1)(STK0)))]
08000	
08100	<PRECONDS>
08200		::=<PC>;				=>[(PROG
08300							    NIL
08400							    (SETQ PRELIST VARLIST)
08500							    (SETQ VARLIST NIL)
08600							    (RETURN(STK1)))]
08700	
08800	<PC>    ::=<C1><PCL>				=>[(CONS(QUOTE THAND)(CONS(STK1)(STK0)))]
08900		::=<C1>					=>*
09000	
09100	<PCL>   ::=<C1><PCL>				=>(C1.PCL)
09200		::=<C1>					=>(C1)
09300	
09400	<C1>    ::=<C>;					=>C
09500	
09600	<C>     ::=<PRED><CL>				=>[(APPEND
09700							    (CONS(QUOTE THOR)(CONS(STK1)(STK0)))
09800							    (QUOTE((CONDSTAT(THV GCL)T))))]
09900		::=<PRED>				=>*
10000		::=(<PC>)				=>*
10100	
10200	<CL>    ::=<PRED><CL>				=>(PRED.CL)
10300		::=<PRED>				=>(PRED)
10400		::=(<PC>)				=>(PC)
10500	
10600	<PRED>  ::=<NOT><LIT>				=>[(COND
10700							    ((EQ(CAR(STK0))(QUOTE =))
10800							     (MAKEQUAL
10900							      (CDR(STK0))
11000							      (CONS(QUOTE EQUAL)(CDR STK0))))
11100							    (T(MAKENOT(STK0))))]
11200		::=<LIT>				=>[(COND
11300							    ((EQ(CAR(STK0))(QUOTE =))
11400							     (MAKEQUAL
11500							      (CDR(STK0))
11600							      (LIST
11700							       (QUOTE NOT)
11800							       (CONS(QUOTE EQUAL)(CDR(STK0))))))
11900							    (T(MAKEPRED(STK0))))]
12000	
12100	<LIT>   ::=<PREDLET><ITMLST>			=>(PREDLET.ITMLST)
12200	
12300	<ITMLST>::=(<ITMS>				=>*
12400	
12500	<ITMS>  ::=<TM2><ITMS>				=>(TM2.ITMS)
12600		::=<TM>)				=>(TM)
12700	
12800	<TM2>   ::=<TM>,				=>*
12900	
13000	<TM>    ::=<IVAR>				=>[(PROG2
13100							    (COND
13200							     ((NOT(MEMQ(STK0)VARLIST))
13300							      (SETQ VARLIST(CONS(STK0)VARLIST))))
13400							    (LIST(QUOTE THV)(STK0)))]
13500		::=<PREFN><ITMLST>			=>(PREFN.ITMLST)
13600		::=<PREFN>				=>(PREFN)
13700	
13800	<POSTCOND>
13900		::=<POSTPRED>;<POSTCOND>		=>(POSTPRED.POSTCOND)
14000		::=;					=>NIL
14100	
14200	<POSTPRED>
14300		::=<NOT><LIT>				=>(NOT.LIT)
14400		::=<LIT>				=>*
14500	
14600	<IVAR>  ::=<ID>					=>*
14700	
14800	<PREFN> ::=<ID>					=>*
14900	
15000	<PREDLET>
15100		::=<ID>					=>*
15200		::==					=>=
15300	
15400	<NOT>   ::=¬					=>¬
15500	
15600	
15700	END
15800	
15900	NIL